(set-logic QF_AUFLIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x_0 () Int)
(declare-fun x_1 () Int)
(declare-fun x_2 () (Array Int Int))
(declare-fun x_3 () Bool)
(declare-fun x_4 (Int) Int)
(declare-fun x_5 () Int)
(declare-fun x_6 () Bool)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Int)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Int)
(declare-fun x_15 () Int)
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 (Int) Int)
(declare-fun x_19 (Int Int Int) Int)
(declare-fun x_20 (Int) Int)
(declare-fun x_21 () Bool)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Int)
(declare-fun x_24 () Int)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Int)
(declare-fun x_27 () Int)
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () Bool)
(declare-fun x_35 () Int)
(declare-fun x_36 () Int)
(declare-fun x_37 () Int)
(declare-fun x_38 () Int)
(declare-fun x_39 () (Array Int Int))
(declare-fun x_40 () Int)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Int)
(declare-fun x_44 () Int)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Int)
(declare-fun x_47 () Int)
(declare-fun x_48 () Int)
(declare-fun x_49 () Int)
(declare-fun x_50 () Int)
(declare-fun x_51 () Bool)
(declare-fun x_52 () Int)
(declare-fun x_53 () Int)
(declare-fun x_54 () Bool)
(declare-fun x_55 () Int)
(declare-fun x_56 () Int)
(declare-fun x_57 () Int)
(declare-fun x_58 () Int)
(declare-fun x_59 () (Array Int Int))
(declare-fun x_60 () Int)
(declare-fun x_61 () Bool)
(declare-fun x_62 () Bool)
(declare-fun x_63 () Int)
(declare-fun x_64 () Int)
(declare-fun x_65 () Bool)
(declare-fun x_66 () Int)
(declare-fun x_67 () Int)
(declare-fun x_68 () Int)
(declare-fun x_69 () Int)
(declare-fun x_70 () Int)
(declare-fun x_71 () Bool)
(declare-fun x_72 () Int)
(declare-fun x_73 () Int)
(declare-fun x_74 () Bool)
(declare-fun x_75 () Int)
(declare-fun x_76 () Int)
(declare-fun x_77 () Int)
(declare-fun x_78 () Int)
(declare-fun x_79 () (Array Int Int))
(declare-fun x_80 () Int)
(declare-fun x_81 () Bool)
(declare-fun x_82 () Bool)
(declare-fun x_83 () Int)
(declare-fun x_84 () Int)
(declare-fun x_85 () Bool)
(declare-fun x_86 () Int)
(declare-fun x_87 () Int)
(declare-fun x_88 () Int)
(declare-fun x_89 () Int)
(declare-fun x_90 () Int)
(declare-fun x_91 () Bool)
(declare-fun x_92 () Int)
(declare-fun x_93 () Int)
(declare-fun x_94 () Bool)
(declare-fun x_95 () Int)
(declare-fun x_96 () Int)
(declare-fun x_97 () Int)
(declare-fun x_98 () Int)
(declare-fun x_99 () (Array Int Int))
(declare-fun x_100 () Int)
(declare-fun x_101 () Bool)
(declare-fun x_102 (Int) Int)
(declare-fun x_103 () (Array Int Int))
(declare-fun x_104 () Int)
(declare-fun x_105 () Int)
(declare-fun x_106 (Int) Int)
(declare-fun x_107 () Int)
(declare-fun x_108 () Int)
(declare-fun x_109 () Int)
(declare-fun x_110 () Int)
(declare-fun x_111 () (Array Int Int))
(declare-fun x_112 () (Array Int Int))
(declare-fun x_113 () (Array Int Int))
(declare-fun x_114 () Int)
(declare-fun x_115 () Int)
(declare-fun x_116 () Int)
(declare-fun x_117 () Int)
(declare-fun x_118 () Int)
(declare-fun x_119 () Int)
(declare-fun x_120 () Int)
(declare-fun x_121 () Int)
(declare-fun x_122 () (Array Int Int))
(declare-fun x_123 () (Array Int Int))
(declare-fun x_124 () (Array Int Int))
(declare-fun x_125 () (Array Int Int))
(declare-fun x_126 () (Array Int Int))
(declare-fun x_127 () Int)
(declare-fun x_128 () Int)
(declare-fun x_129 () Int)
(declare-fun x_130 () (Array Int Int))
(declare-fun x_131 () (Array Int Int))
(declare-fun x_132 () Int)
(declare-fun x_133 () Int)
(declare-fun x_134 () Int)
(declare-fun x_135 () Int)
(declare-fun x_136 () (Array Int Int))
(declare-fun x_137 () (Array Int Int))
(declare-fun x_138 () (Array Int Int))
(declare-fun x_139 () Int)
(declare-fun x_140 () Int)
(declare-fun x_141 () Int)
(declare-fun x_142 () (Array Int Int))
(declare-fun x_143 () (Array Int Int))
(declare-fun x_144 () Int)
(declare-fun x_145 () Int)
(declare-fun x_146 () Int)
(declare-fun x_147 () Int)
(declare-fun x_148 () (Array Int Int))
(declare-fun x_149 () (Array Int Int))
(declare-fun x_150 () Int)
(declare-fun x_151 () Int)
(declare-fun x_152 () Int)
(declare-fun x_153 () Int)
(declare-fun x_154 () Int)
(declare-fun x_155 () Int)
(declare-fun x_156 () Int)
(declare-fun x_157 () Int)
(declare-fun x_158 () Int)
(declare-fun x_159 () Int)
(assert (let ((?v_1 (and x_62 (= (x_4 x_63) x_64))) (?v_2 (not (= x_70 0))) (?v_4 (and x_71 (= (x_4 x_72) x_73))) (?v_5 (= x_70 2)) (?v_6 (= x_70 3)) (?v_7 (x_4 x_43))) (let ((?v_9 (and x_42 (= ?v_7 x_44))) (?v_10 (not (= x_50 0))) (?v_12 (x_4 x_52))) (let ((?v_14 (and x_51 (= ?v_12 x_53))) (?v_11 (= x_50 2)) (?v_15 (= x_50 3)) (?v_16 (x_4 x_23))) (let ((?v_18 (and x_22 (= ?v_16 x_24))) (?v_19 (not (= x_30 0))) (?v_21 (x_4 x_32))) (let ((?v_23 (and x_31 (= ?v_21 x_33))) (?v_20 (= x_30 2)) (?v_24 (= x_30 3)) (?v_26 (x_4 x_1))) (let ((?v_28 (and x_3 (= ?v_26 x_5))) (?v_25 (= x_0 0))) (let ((?v_29 (not ?v_25)) (?v_34 (and x_11 (= ?v_26 x_12))) (?v_30 (= x_0 2)) (?v_35 (= x_0 3)) (?v_27 (x_18 x_1)) (?v_17 (x_18 x_23)) (?v_22 (x_18 x_32)) (?v_8 (x_18 x_43)) (?v_13 (x_18 x_52)) (?v_0 (x_18 x_63)) (?v_3 (x_18 x_72)) (?v_36 (ite x_65 (store x_138 x_66 x_68) x_138)) (?v_37 (ite ?v_5 x_83 x_141))) (let ((?v_38 (ite ?v_5 ?v_36 x_142)) (?v_31 (x_102 x_1)) (?v_32 (x_20 x_1)) (?v_33 (x_106 x_1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (< x_0 0)) (not (< x_30 0))) (not (< x_50 0))) (not (< x_70 0))) (not (< x_90 0))) ?v_25) x_101) x_81) x_61) x_41) x_21) (= x_90 (+ x_70 1))) (= x_83 (ite (or ?v_2 ?v_1) x_63 (x_102 x_63)))) (= x_87 ?v_0)) (= x_89 (select ?v_36 ?v_0))) (= x_84 (x_106 x_63))) (= x_82 (and (not ?v_1) (not ?v_2)))) (= x_88 (x_19 x_139 x_140 (ite (and x_65 (= x_66 x_67)) x_68 x_69)))) (= x_86 x_64)) (= x_85 x_62)) (= x_92 (ite (or x_81 ?v_4) x_72 (x_102 x_72)))) (= x_96 ?v_3)) (= x_98 (select (ite x_74 (store x_143 x_75 x_77) x_143) ?v_3))) (= x_93 (x_106 x_72))) (= x_91 (and (not ?v_4) (not x_81)))) (= x_97 (x_19 x_144 x_145 (ite (and x_74 (= x_75 x_76)) x_77 x_78)))) (= x_95 x_73)) (= x_94 x_71)) (= x_100 (ite ?v_5 x_72 (ite ?v_6 (x_102 x_80) x_80)))) (= x_99 (ite ?v_5 x_143 (ite ?v_6 (store x_79 (x_106 x_80) (x_19 (x_20 x_80) (select x_79 (x_4 x_80)) (select x_79 (x_18 x_80)))) x_79)))) (= x_70 (+ x_50 1))) (= x_63 (ite (or ?v_10 ?v_9) x_43 (x_102 x_43)))) (= x_138 (ite x_45 (store x_126 x_46 x_48) x_126))) (= x_139 (x_20 x_43))) (= x_67 ?v_8)) (= x_140 (select x_138 ?v_7))) (= x_69 (select x_138 ?v_8))) (= x_64 (x_106 x_43))) (= x_62 (and (not ?v_9) (not ?v_10)))) (= x_68 (x_19 x_127 x_128 (ite (and x_45 (= x_46 x_47)) x_48 x_49)))) (= x_66 x_44)) (= x_65 x_42)) (= x_141 (ite ?v_11 x_63 x_129))) (= x_142 (ite ?v_11 x_138 x_130))) (= x_72 (ite (or x_61 ?v_14) x_52 (x_102 x_52)))) (= x_143 (ite x_54 (store x_131 x_55 x_57) x_131))) (= x_144 (x_20 x_52))) (= x_76 ?v_13)) (= x_145 (select x_143 ?v_12))) (= x_78 (select x_143 ?v_13))) (= x_73 (x_106 x_52))) (= x_71 (and (not ?v_14) (not x_61)))) (= x_77 (x_19 x_132 x_133 (ite (and x_54 (= x_55 x_56)) x_57 x_58)))) (= x_75 x_53)) (= x_74 x_51)) (= x_80 (ite ?v_11 x_52 (ite ?v_15 (x_102 x_60) x_60)))) (= x_79 (ite ?v_11 x_131 (ite ?v_15 (store x_59 (x_106 x_60) (x_19 (x_20 x_60) (select x_59 (x_4 x_60)) (select x_59 (x_18 x_60)))) x_59)))) (= x_146 (ite ?v_11 x_80 x_134))) (= x_147 (ite ?v_15 x_80 x_135))) (= x_148 (ite ?v_11 x_79 x_136))) (= x_149 (ite ?v_15 x_79 x_137))) (= x_50 (+ x_30 1))) (= x_43 (ite (or ?v_19 ?v_18) x_23 (x_102 x_23)))) (= x_126 (ite x_25 (store x_103 x_26 x_28) x_103))) (= x_127 (x_20 x_23))) (= x_47 ?v_17)) (= x_128 (select x_126 ?v_16))) (= x_49 (select x_126 ?v_17))) (= x_44 (x_106 x_23))) (= x_42 (and (not ?v_18) (not ?v_19)))) (= x_48 (x_19 x_104 x_105 (ite (and x_25 (= x_26 x_27)) x_28 x_29)))) (= x_46 x_24)) (= x_45 x_22)) (= x_129 (ite ?v_20 x_43 x_109))) (= x_130 (ite ?v_20 x_126 x_111))) (= x_52 (ite (or x_41 ?v_23) x_32 (x_102 x_32)))) (= x_131 (ite x_34 (store x_113 x_35 x_37) x_113))) (= x_132 (x_20 x_32))) (= x_56 ?v_22)) (= x_133 (select x_131 ?v_21))) (= x_58 (select x_131 ?v_22))) (= x_53 (x_106 x_32))) (= x_51 (and (not ?v_23) (not x_41)))) (= x_57 (x_19 x_114 x_115 (ite (and x_34 (= x_35 x_36)) x_37 x_38)))) (= x_55 x_33)) (= x_54 x_31)) (= x_60 (ite ?v_20 x_32 (ite ?v_24 (x_102 x_40) x_40)))) (= x_59 (ite ?v_20 x_113 (ite ?v_24 (store x_39 (x_106 x_40) (x_19 (x_20 x_40) (select x_39 (x_4 x_40)) (select x_39 (x_18 x_40)))) x_39)))) (= x_134 (ite ?v_20 x_60 x_118))) (= x_135 (ite ?v_24 x_60 x_120))) (= x_136 (ite ?v_20 x_59 x_122))) (= x_137 (ite ?v_24 x_59 x_124))) (= x_30 (+ x_0 1))) (= x_23 (ite (or ?v_29 ?v_28) x_1 ?v_31))) (= x_103 (ite x_6 (store x_2 x_7 x_9) x_2))) (= x_104 ?v_32)) (= x_27 ?v_27)) (= x_105 (select x_103 ?v_26))) (= x_29 (select x_103 ?v_27))) (= x_24 ?v_33)) (= x_22 (and (not ?v_28) (not ?v_29)))) (= x_28 (x_19 x_107 x_108 (ite (and x_6 (= x_7 x_8)) x_9 x_10)))) (= x_26 x_5)) (= x_25 x_3)) (= x_109 (ite ?v_30 x_23 x_110))) (= x_111 (ite ?v_30 x_103 x_112))) (= x_32 (ite (or x_21 ?v_34) x_1 ?v_31))) (= x_113 (ite x_13 (store x_2 x_14 x_16) x_2))) (= x_114 ?v_32)) (= x_36 ?v_27)) (= x_115 (select x_113 ?v_26))) (= x_38 (select x_113 ?v_27))) (= x_33 ?v_33)) (= x_31 (and (not ?v_34) (not x_21)))) (= x_37 (x_19 x_116 x_117 (ite (and x_13 (= x_14 x_15)) x_16 x_17)))) (= x_35 x_12)) (= x_34 x_11)) (= x_40 (ite ?v_30 x_1 (ite ?v_35 ?v_31 x_1)))) (= x_39 (ite ?v_30 x_2 (ite ?v_35 (store x_2 ?v_33 (x_19 ?v_32 (select x_2 ?v_26) (select x_2 ?v_27))) x_2)))) (= x_118 (ite ?v_30 x_40 x_119))) (= x_120 (ite ?v_35 x_40 x_121))) (= x_122 (ite ?v_30 x_39 x_123))) (= x_124 (ite ?v_35 x_39 x_125))) (or (or (or (or (and (and (not (<= x_90 3)) (or (not (= (ite ?v_6 x_100 x_147) ?v_37)) (not (= (select (ite ?v_6 x_99 x_149) x_150) (select ?v_38 x_150))))) (or (not (= (ite ?v_5 x_100 x_146) ?v_37)) (not (= (select (ite ?v_5 x_99 x_148) x_151) (select ?v_38 x_151))))) (and (and (not (<= x_70 3)) (or (not (= x_147 x_141)) (not (= (select x_149 x_152) (select x_142 x_152))))) (or (not (= x_146 x_141)) (not (= (select x_148 x_153) (select x_142 x_153)))))) (and (and (not (<= x_50 3)) (or (not (= x_135 x_129)) (not (= (select x_137 x_154) (select x_130 x_154))))) (or (not (= x_134 x_129)) (not (= (select x_136 x_155) (select x_130 x_155)))))) (and (and (not (<= x_30 3)) (or (not (= x_120 x_109)) (not (= (select x_124 x_156) (select x_111 x_156))))) (or (not (= x_118 x_109)) (not (= (select x_122 x_157) (select x_111 x_157)))))) (and (and (not (<= x_0 3)) (or (not (= x_121 x_110)) (not (= (select x_125 x_158) (select x_112 x_158))))) (or (not (= x_119 x_110)) (not (= (select x_123 x_159) (select x_112 x_159))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
